Nuprl Lemma : qadd_grp_wf 11,40

qadd_grp  abgrp{i:l} 
latex


Definitionst.2, t.1, grp_op(g), grp_car(g), comm(Top), inverse(Topidinv), ident(Topid), assoc(Top), P  Q, xt(x), P  Q, prop{i:l}, P  Q, x f y, P  Q, x:AB(x), eqfun_p(Teq), qadd_grp, abgrp{i:l}, t  T, x(s), mon{i:l}, grp{i:l}, subtype(ST)
Lemmasqadd minus, qadd ident, qadd com, qadd assoc, assert-qeq, iff functionality wrt iff, assert wf, iff wf, all functionality wrt iff, qmul wf, int inc rationals, qadd wf, q le wf, qeq wf2, rationals wf, mk grp, grp op wf, grp car wf, comm wf

origin